package no.uio.ifi.cop.prover.rete;

import java.util.LinkedList;
import no.uio.ifi.cop.common.Log;
/// import no.uio.ifi.cop.cl.Axiom;
/// import no.uio.ifi.cop.cl.Term;
/// import no.uio.ifi.cop.cl.Conjunction;
/// import no.uio.ifi.cop.cl.Predicate;
import no.uio.ifi.cop.cl.Substitution;


/**
 * Represents an Beta node in the RETE matching scheme.
 *
 * An Alpha node has pointers to each of its Beta nodes,
 * where the Beta nodes represents an occurrence of the
 * predicate which the Alpha node represents. So each time
 * an Alpha nodes matches a new fact, the Beta nodes are 
 * notified, if the Beta node has 'siblings', i.e. they
 * are part of a conjunction, their neighbours are also
 * notified about the match. If their neighbours have matches
 * as well, we may have located a matching substitution for
 * the entire left side of a formula. To figure out whether
 * this is true, we take the cross-product of the newly matched
 * predicate, and each of the siblings matches.
 *
 * @version 1.0
 * @author bjarneh@ifi.uio.no
 */


public final class BetaNode implements Cloneable{

    AlphaNode alpha;
    BetaNode parent = null;
    BetaNode child  = null;

    int id; // which rule do I belong to
    int matched;

    BetaNode(AlphaNode a, int identifier){
        alpha = a;
        matched = -1;
        id = identifier;
    }

    private BetaNode(int ident, int match){
        matched = match;
        id = ident;
    }


    public void addParent(BetaNode p){
        parent = p;
        parent.child = this;
    }

    public void fetch(LinkedList<Integer> il, LinkedList<Substitution> sl){
        sl.addFirst( alpha.get( il.pollLast() ) );
        if( parent != null ){
            parent.fetch( il, sl );
        }
    }

    // called once a match has been made
    public MatchList match(){

        // take cross-product of this element with
        // all elements prior and after 
        matched++;

        MatchList matchList = new MatchList();

        matchList.setId( id ); // id of rule that matches

        if( parent != null ){
            if( ! parent.addFirst( matchList ) ){
                return null;
            }
        }

        // add my self as immutable element (unchangeable)
        matchList.setSingle( matchList.size() );
        matchList.addLast( matched );

        if( child != null ){
            if( ! child.addLast( matchList ) ){
                return null;
            }
        }

        // freeze it to block new additions
        matchList.freeze();

        //System.out.println(" alpha: "+ alpha);

        return matchList;
    }


    public boolean addFirst(MatchList list){
        if( matched >= 0 ){
            list.addFirst( matched ); // autobox
            if( parent != null ){
                return parent.addFirst(list);
            }
            return true;
        }
        return false;
    }

    public boolean addLast(MatchList list){
        if( matched >= 0 ){
            list.addLast( matched ); // autobox
            if( child != null ){
                return child.addLast(list);
            }
            return true;
        }
        return false;
    }

    public void addAlpha(LinkedList<AlphaNode> alphas){

        if( alphas.size() == 0 ){ Log.fatal(" alphas.size() == 0 "); }

        alpha = alphas.pollLast();
        alpha.addBeta( this );

        if( parent != null ){
            parent.addAlpha( alphas );
        }
    }

    public void infoString(StringBuilder sb){
        if(parent != null){
            parent.infoString( sb );
        }
        alpha.infoString( sb );
    }

    public BetaNode clone(){
        BetaNode cp = new BetaNode( id, matched );
        if( parent != null ){
            BetaNode cp_parent = parent.clone();
            cp.addParent( cp_parent );
        }
        return cp;
    }

    public String toString(){
        return String.format("@BetaNode( %s )", alpha);
    }

}
